A static analysis technique for defects detection in an application code has been widely used in practice for ensuring software quality and reliability. Initially, the application code may be analyzed using the static analysis, performed by static analysis tools, to generate one or more static analysis warnings. These warnings are generated and reported to user by the analysis tools when the tools are unable to decide about the safety at the program points corresponding to the warnings. In practice, many times, a large portion of the warnings are falsely generated due to the approximations used by the static analysis tools, and they are referred to as false positives. Manual review of the static analysis warnings may be inevitable to fulfill the practical needs of constructing trusted software by identifying manually the false positives and true errors from the static analysis warnings reported by a static analysis tool. Since the review is performed manually, there is a high cost associated with the manual reviewing process. The cost of manual review may be reduced by increasing precision of the static analysis results, or identifying and eliminating automatically the false positives from the static analysis warnings.
Model checking is more precise in property verification as compared to static analysis. However, the model checking of a larger code fragments often faces scalability and poor performance issues as the size and complexity of software systems increases. These issues are faced by model checker due to the state space explosion.
The model checking and the static analysis are well-known techniques for finding warnings in application code. These two techniques have proven to be valuable in practice for ensuring software quality and reliability but they are complementary on the metrics of scalability, precision and efficiency.
The techniques, static analysis and model checking, being complementary can be combined together to achieve better results than the results obtained by them in isolation. The model checker may be used in cascade with static analysis to eliminate the false positives generated by the static analysis.
An incremental approach is used to address the issue of non-scalability of the model checkers on a very large code application. This approach starts with the minimal code context and later increases the context if needed and it has been found to be useful in practice. In this approach, the model checking of the assertion starts with a small calling context in which variables receiving values from outside the context are modelled to take any arbitrary value. The variables taking such values from outside the context are called as input variables. The input variables may be initialized by generating arbitrary values through non-deterministic choice functions. A calling context may be expanded on a need basis to include callers higher up in the call chains. While this calling context aids scalability by keeping the calling context as small as possible, it may require multiple calls to the model checker for the same assertion which increases the time required to process an assertion using model checking. Incremental expansion of the calling contexts may be required when the model checking in a smaller context finds a counterexample. The counterexample generated may not be because of the values assigned to variables by the statements in the program code but it might be because of the non-deterministic choice functions introduced outside of the context to generate arbitrary values to the corresponding input variables. That is, when the variables involved in an assertion are allowed to take any arbitrary value at the point of assertion, that are generated by the non-deterministic choice functions, the assertion may be violated by some or the other combination of values. In such cases, using the model checker may not aid in resolution of the corresponding warning and hence the assertion verification is redundant.
Accordingly, the present system and method describes static analysis-based efficient elimination of one or more false positives from static analysis warnings generated during the property verification.